%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/


%% Created for James Bridge at 2014-09-30 16:26:43 +0100 


%% Saved with string encoding Unicode (UTF-8) 

@inproceedings{MT,
 author = {Akbarpour, Behzad and Paulson, Lawrence C.},
 title = {MetiTarski: An Automatic Prover for the Elementary Functions},
 booktitle = {Proceedings of the 9th AISC International Conference, the 15th Calculemas Symposium, and the 7th International MKM Conference on Intelligent Computer Mathematics},
 year = {2008},
 isbn = {978-3-540-85109-7},
 location = {Birmingham, UK},
 pages = {217--231},
 numpages = {15},
 url = {http://dx.doi.org/10.1007/978-3-540-85110-3_18},
 doi = {10.1007/978-3-540-85110-3_18},
 acmid = {1428611},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}

@incollection{KBO_ext,
year={2007},
isbn={978-3-540-75558-6},
booktitle={Logic for Programming, Artificial Intelligence, and Reasoning},
volume={4790},
series={Lecture Notes in Computer Science},
editor={Dershowitz, Nachum and Voronkov, Andrei},
doi={10.1007/978-3-540-75560-9_26},
title={An Extension of the Knuth-Bendix Ordering with LPO-Like Properties},
url={http://dx.doi.org/10.1007/978-3-540-75560-9_26},
publisher={Springer Berlin Heidelberg},
author={Ludwig, Michel and Waldmann, Uwe},
pages={348-362},
language={English}
}

@inproceedings{SPASS_Splitting,
	Acmid = {1431162},
	Address = {Berlin, Heidelberg},
	Author = {Fietzke, Arnaud and Weidenbach, Christoph},
	Booktitle = {Proceedings of the 4th International Joint Conference on Automated Reasoning},
	Date-Added = {2014-09-24 14:44:51 +0000},
	Date-Modified = {2014-09-26 10:46:41 +0000},
	Doi = {10.1007/978-3-540-71070-7_39},
	Isbn = {978-3-540-71069-1},
	Location = {Sydney, Australia},
	Numpages = {16},
	Pages = {459--474},
	Publisher = {Springer-Verlag},
	Series = {IJCAR '08},
	Title = {Labelled Splitting},
	Url = {http://dx.doi.org/10.1007/978-3-540-71070-7_39},
	Year = {2008},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-71070-7_39}}

@article{MT_Splitting,
	Author = {Bridge, James P. and Paulson, Lawrence Charles},
	Date-Modified = {2014-09-26 10:46:00 +0000},
	Doi = {10.1007/s10817-012-9245-6},
	Issn = {0168-7433},
	Journal = {Journal of Automated Reasoning},
	Keywords = {Splitting; Resolution theorem proving; SPASS; MetiTarski},
	Language = {English},
	Number = {1},
	Pages = {99-117},
	Publisher = {Springer Netherlands},
	Title = {Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions},
	Url = {http://dx.doi.org/10.1007/s10817-012-9245-6},
	Volume = {50},
	Year = {2013},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/s10817-012-9245-6}}

@ARTICLE{McCune90,
    author = {William McCune},
    title = {Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval},
    journal = {JOURNAL OF AUTOMATED REASONING},
    year = {1990},
    volume = {9},
    pages = {9--2}
}